LeanMachineLearning exposition

Bandits.«term𝓛[_|_In_;_]»🔗

Minimal Lean file

term𝓛[_|_In_;_]🔗

DefinitionBandits.«term𝓛[_|_In_;_]»
Details

Law of Y conditioned on the event that X is in s.

🔗def
Bandits.«term𝓛[_|_In_;_]» : Lean.ParserDescr
Bandits.«term𝓛[_|_In_;_]» :
  Lean.ParserDescr

Code

notation "𝓛[" Y " | " X " in " s "; " μ "]" => Measure.map Y (μ[|X ⁻¹' s])

Actions: Source · Open Issue